Abstract
Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the flow of values through them. The article presents the algorithms that we developed, explains how they are used to recover Intermediate Representations (IRs) from executables that are similar to the IRs that would be available if one started from source code, and describes their application in the context of program understanding and automated bug hunting.
Unlike algorithms for analyzing executables that existed prior to our work, the ones presented in this article provide useful information about memory accesses, even in the absence of debugging information. The ideas described in the article are incorporated in a tool for analyzing Intel x86 executables, called CodeSurfer/x86. CodeSurfer/x86 builds a system dependence graph for the program, and provides a GUI for exploring the graph by (i) navigating its edges, and (ii) invoking operations, such as forward slicing, backward slicing, and chopping, to discover how parts of the program can impact other parts.
To assess the usefulness of the IRs recovered by CodeSurfer/x86 in the context of automated bug hunting, we built a tool on top of CodeSurfer/x86, called Device-Driver Analyzer for x86 (DDA/x86), which analyzes device-driver executables for bugs. Without the benefit of either source code or symbol-table/debugging information, DDA/x86 was able to find known bugs (that had been discovered previously by source-code analysis tools), along with useful error traces, while having a low false-positive rate. DDA/x86 is the first known application of program analysis/verification techniques to industrial executables.
- Aigner, G. and Hölzle, U. 1996. Eliminating virtual function calls in C++ programs. In Proceedings of the European Conference on Object-Oriented Programming. Google ScholarDigital Library
- aiT. aiT worst-case execution time analyzer. http://www.AbsInt.com/aiT.Google Scholar
- Amme, W., Braun, P., Zehendner, E., and Thomasset, F. 2000. Data dependence analysis of assembly code. Int. J. Parall. Program. 28, 5, 431--467. Google ScholarDigital Library
- Backes, W. 2004. Programmanalyse des xrtl zwischencodes. Ph.D. thesis, Universitaet des Saarlandes. (In German.)Google Scholar
- Bala, V., Duesterwald, E., and Banerjia, S. 2000. Dynamo: A transparent runtime optimization system. In Proceedings of the Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- Balakrishnan, G. 2007. WYSINWYX: What You See Is Not What You eXecute. Ph.D. thesis, Tech. rep. 1603. Computer Science Department, University of Wisconsin, Madison, WI. Google ScholarDigital Library
- Balakrishnan, G., Gruian, R., Reps, T., and Teitelbaum, T. 2005a. Codesurfer/x86 -- A platform for analyzing x86 executables, (tool demonstration paper). In Proceedings of the International Conference on Compiler Construction. Google ScholarDigital Library
- Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction. 5--23.Google Scholar
- Balakrishnan, G. and Reps, T. 2006. Recency-Abstraction for heap-allocated storage. In Proceedings of the Static Analysis Symposium. Google ScholarDigital Library
- Balakrishnan, G. and Reps, T. 2007. DIVINE: DIscovering Variables IN Executables. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. Google ScholarDigital Library
- Balakrishnan, G. and Reps, T. 2008. Analyzing stripped device-driver executables. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. Google ScholarDigital Library
- Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., and Teitelbaum, T. 2005b. Model checking x86 executables with CodeSurfer/x86 and WPDS++. In Proceedings of the Conference on Computer Aided Verification. Google ScholarDigital Library
- Balakrishnan, G., Reps, T., Melski, D., and Teitelbaum, T. 2007. WYSINWYX: What you see is not what you execute. In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments.Google Scholar
- Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S., and Ustuner, A. 2006. Thorough static analysis of device drivers. In Proceedings of the European Conference on Computer Systems. Google ScholarDigital Library
- Ball, T. and Rajamani, S. 2000. Bebop: A symbolic model checker for Boolean programs. In Proceedings of the Spin Workshop. Lecture Notes in Computer Science, vol. 1885. Springer, 113--130. Google ScholarDigital Library
- Ball, T. and Rajamani, S. 2001. The SLAM toolkit. In Proceedings of the Conference on Computer-Aided Verification. Google ScholarDigital Library
- Bergeron, J., Debbabi, M., Desharnais, J., Erhioui, M., Lavoie, Y., and Tawbi, N. 2001. Static detection of malicious code in executable programs. Int. J. Req. Engin.Google Scholar
- Bergeron, J., Debbabi, M., Erhioui, M., and Ktari, B. 1999. Static analysis of binary code to isolate malicious behaviors. In Proceedings of the International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises. Google ScholarDigital Library
- Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2003. A static analyzer for large safety-critical software. In Proceedings of the Conference on Programming Language Design and Implementation. 196--207. Google ScholarDigital Library
- Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model checking. In Proceedings of the International Conference on Concurrency Theory (CONCUR'97). Google ScholarDigital Library
- Bourdoncle, F. 1993. Efficient chaotic iteration strategies with widenings. In Proceedings of the International Conference on Formal Methods in Programming and Their Application. Lecture Notes in Computer Science. Springer.Google Scholar
- Brown, R., Khazan, R., and Zhivich, M. 2007. AWE: Improving software analysis through modular integration of static and dynamic analyses. In Workshop on Program Analysis for Software Tools and Engineering (PASTE'07). Google ScholarDigital Library
- Brumley, D. and Newsome, J. 2006. Alias analysis for assembly. Tech. rep. CMU-CS-06-180, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.Google Scholar
- Bryant, R. 1986. Graph-Based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35, 6, 677--691. Google ScholarDigital Library
- Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the Symposium on Logic in Computer Science. 428--439.Google Scholar
- Bush, W., Pincus, J., and Sielaff, D. 2000. A static analyzer for finding dynamic programming errors. Softw. Pract. Exper. 30, 775--802. Google ScholarDigital Library
- Cai, H., Shao, Z., and Vaynberg, A. 2007. Certified self-modifying code. In Proceedings of the Conference on Programming Language Design and Implementation. ACM Press, New York, 66--77. Google ScholarDigital Library
- Chandra, S. and Reps, T. 1999. Physical type checking for C. In Proceedings of the Conference on Program Analysis for Software Tools and Engineering. 66--75. Google ScholarDigital Library
- Chang, B.-Y., Harren, M., and Necula, G. 2006. Analysis of low-level code using cooperating decompilers. In Proceedings of the Static Analysis Symposium. Google ScholarDigital Library
- Chen, H. and Wagner, D. 2002. MOPS: An infrastructure for examining security properties of software. In Proceedings of the Conference on Computer and Communications Security. 235--244. Google ScholarDigital Library
- Chou, A., Yang, J., Chelf, B., Hallem, S., and Engler, D. 2001. An empirical study of operating systems errors. In Proceedings of the Symposium on Operating Systems Principles. Google ScholarDigital Library
- Christodorescu, M., Goh, W.-H., and Kidd, N. 2005. String analysis for x86 binaries. In Proceedings of the Conference on Program Analysis for Software Tools and Engineering. Google ScholarDigital Library
- Cifuentes, C. and Fraboulet, A. 1997a. Interprocedural data flow recovery of high-level language code from assembly. Tech. rep. 421, University of Queensland.Google Scholar
- Cifuentes, C. and Fraboulet, A. 1997b. Intraprocedural static slicing of binary executables. In Proceedings of the International Conference on Software Maintenance. 188--195. Google ScholarDigital Library
- Cifuentes, C., Simon, D., and Fraboulet, A. 1998. Assembly to high-level language translation. In Proceedings of the International Conference on Software Maintenance. 228--237. Google ScholarDigital Library
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-Guided abstraction refinement. In Proceedings of the Conference on Computer Aided Verification. 154--169. Google ScholarDigital Library
- CodeSonar. CodeSonar, GrammaTech, Inc. www.grammatech.com/products/codesonar.Google Scholar
- CodeSurfer. CodeSurfer, GrammaTech, Inc. www.grammatech.com/products/codesurfer.Google Scholar
- Cooper, K. and Kennedy, K. 1988. Interprocedural side-effect analysis in linear time. In Proceedings of the Conference on Program Language Design and Implementation. 57--66. Google ScholarDigital Library
- Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In Proceedings of the International Conference on Software Engineering. 439--448. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the Symposium on Principles of Programming Language. 238--252. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the Symposium on Principles of Programming Language. 269--282. Google ScholarDigital Library
- Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear constraints among variables of a program. In Proceedings of the Symposium on Principles of Programming Language. 84--96. Google ScholarDigital Library
- Cova, M., Felmetsger, V., Banks, G., and Vigna, G. 2006. Static detection of vulnerabilities in x86 executables. In Proceedings of the Annual Computer Security Applications Conference. Google ScholarDigital Library
- Coverity. Coverity Prevent. www.coverity.com/html/coverity-prevent-static-analysis.html.Google Scholar
- Das, M., Lerner, S., and Seigle, M. 2002. ESP: Path-Sensitive program verification in polynomial time. In Proceedings of the Conference on Programming Language Design and Implementation. ACM Press, New York, 57--68. Google ScholarDigital Library
- De Sutter, B., De Bus, B., De Bosschere, K., Keyngnaert, P., and Demoen, B. 2000. On the static analysis of indirect control transfers in binaries. In Proceedings of the International Confernece on Parallel and Distributed Processing Techniques and Applications.Google Scholar
- Debray, S., Linn, C., Andrews, G., and Schwarz, B. 2004. Stack analysis of x86 executables. www.cs.arizona.edu/~debray/Publications/stack-analysis.pdf.Google Scholar
- Debray, S., Muth, R., and Weippert, M. 1998. Alias analysis of executable code. In Proceedings of the Symposium on Principles of Programming Language. 12--24. Google ScholarDigital Library
- Dhurjati, D., Das, M., and Yang, Y. 2006. Path-Sensitive dataflow analysis with iterative refinement. In Proceedings of the Static Analysis Symposium. 425--442. Google ScholarDigital Library
- DMCA §1201. §1201. Circumvention of Copyright Protection Systems. www.copyright.gov/title17/92chap12.html#1201.Google Scholar
- Dor, N., Rodeh, M., and Sagiv, M. 2003. CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. In Proceedings of the Conference on Program Language Design and Implementation. 155--167. Google ScholarDigital Library
- Eidorff, P., Henglein, F., Mossin, C., Niss, H., Sørensen, M., and Tofte, M. 1999. Anno Domini: From type theory to year 2000 conversion tool. In Proceedings of the Symposium on Principles of Programming Language. 1--14. Google ScholarDigital Library
- Emmerik, M. V. 2007. Static single assignment for decompilation. Ph.D. thesis, School of Information Technology and Electrical Engineering, University of Queensland, Brisbane, Australia.Google Scholar
- Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Conference on Operating System Design and Implementation. 1--16. Google ScholarDigital Library
- Feng, X., Shao, Z., Vaynberg, A., Xiang, S., and Ni, Z. 2006. Modular verification of as - sembly code with stack-based control abstractions. In Proceedings of the Conference on Program Language Design and Implementation. 401--414. Google ScholarDigital Library
- Ferdinand, C. 2009. Personal communication.Google Scholar
- Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., and Wilhelm, R. 2001. Reliable and precise WCET determination for a real-life processor. In Proceedings of the 1st International Workshop on Embedded Software (EMSOFT'01). 469--485. Google ScholarDigital Library
- Finkel, A., Willems, B., and Wolper, P. 1997. A direct symbolic approach to model checking pushdown systems. Elec. Not. Theor. Comput. Sci. 9.Google Scholar
- Fischer, J., Jhala, R., and Majumdar, R. 2005. Joining dataflow with predicates. In Proceedings of the Conference on Foundations of Software Engineering. Google ScholarDigital Library
- Gopan, D. and Reps, T. 2006. Lookahead widening. In Proceedings of the Conference on Computer Aided Verification. Google ScholarDigital Library
- Gopan, D. and Reps, T. 2007. Low-Level library analysis and summarization. In Proceedings of the Conference on Computer Aided Verification. Google ScholarDigital Library
- Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer, 72--83. Google ScholarDigital Library
- Grewe, D. 2008. Static congruence analysis of binaries. Bachelors thesis, University des Saarlandes.Google Scholar
- Guo, B., Bridges, M., Triantafyllis, S., Ottoni, G., Raman, E., and August, D. 2005. Practical and accurate low-level pointer analysis. In Proceedings of the 3rd International Symposium on Code Generation and Optimization. 291--302. Google ScholarDigital Library
- Halbwachs, N., Proy, Y.-E., and Roumanoff, P. 1997. Verification of real-time systems using linear relation analysis. Formal Methods Syst. Des. 11, 2, 157--185. Google ScholarDigital Library
- Havelund, K. and Pressburger, T. 2000. Model checking Java programs using Java PathFinder. Softw. Tools Tech. Transfer 2, 4.Google ScholarCross Ref
- Henzinger, T., Jhala, R., Majumdar, R., and McMillan, K. L. 2004. Abstractions from proofs. In Proceedings of the Symposium on Principles of Programming Language. 232--244. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the Symposium on Principles of Programming Language. 58--70. Google ScholarDigital Library
- Hind, M. 2001. Pointer analysis: Haven't we solved this problem yet? In Proceedings of the Conference on Program Analysis for Software Tools and Engineering. Google ScholarDigital Library
- Holley, L. and Rosen, B. 1981. Qualified data flow problems. Trans. Softw. Engin. 7, 1, 60--78. Google ScholarDigital Library
- Howard, M. 2002. Some bad news and some good news. MSDN, Microsoft Corp., msdn2.microsoft.com/en-us/library/ms972826.aspx.Google Scholar
- IDAPro. IDAPro disassembler. www.hex-rays.com/idapro/.Google Scholar
- Kiriansky, V., Bruening, D., and Amarasinghe, S. 2002. Secure execution via program shepherding. In Proceedings of the USENIX Security Symposium. Google ScholarDigital Library
- Kiss, A., J. Jász, G. L., and Gyimóthy, T. 2003. Interprocedural static slicing of binary executables. In Proceedings of the International Workshop on Source Code Analysis and Manipulation.Google Scholar
- Kruegel, C., Kirda, E., Mutz, D., Robertson, W., and Vigna, G. 2005. Automating mimicry attacks using static binary analysis. In Proceedings of the USENIX Security Symposium. Google ScholarDigital Library
- Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press. Google ScholarDigital Library
- Lal, A., Reps, T., and Balakrishnan, G. 2005. Extended weighted pushdown systems. In Proceedings of the Conference on Computer Aided Verification. Google ScholarDigital Library
- Larus, J. and Schnarr, E. 1995. EEL: Machine-Independent executable editing. In Proceedings of the Conference on Programming Language Design and Implementation. 291--300. Google ScholarDigital Library
- Lim, J. and Reps, T. 2008. A system for generating static analyzers for machine instructions. In Proceedings of the International Conference on Compiler Construction. Google ScholarDigital Library
- Lim, J., Reps, T., and Liblit, B. 2006. Extracting output formats from executables. In Proceedings of the Working Conference on Reverse Engineering. Google ScholarDigital Library
- Manevich, R., Ramalingam, G., Field, J., Goyal, D., and Sagiv, M. 2002. Compactly representing first-order structures for static analysis. In Proceedings of the Static Analysis Symposium. 196--212. Google ScholarDigital Library
- Mauborgne, L. and Rival, X. 2005. Trace partitioning in abstract interpretation based static analyzers. In Proceedings of the European Symposium on Programming. Google ScholarDigital Library
- Miné, A. 2006. Field-Sensitive value analysis of embedded C programs with union types and pointer arithmetics. In Proceedings of the Conference on Languages, Compilers, and Tools for Embedded Systems. Google ScholarDigital Library
- Müller-Olm, M. and Seidl, H. 2005. Analysis of modular arithmetic. In Proceedings of the European Symposium on Programming. Google ScholarDigital Library
- Mycroft, A. 1999. Type-Based decompilation. In Proceedings of the European Symposium on Programming.Google Scholar
- Myers, E. 1984. Efficient applicative data types. In Proceedings of the Symposium on Principles of Programming Languages. Google ScholarDigital Library
- Ni, Z. and Shao, Z. 2006. Certified assembly programming with embedded code pointers. In Proceedings of the Symposium on Principles of Programming Languages. 320--333. Google ScholarDigital Library
- Nita, M., Grossman, D., and Chambers, C. 2008. A theory of platform-dependent low-level software. In Proceedings of the Symposium on Principles of Programming Languages. Google ScholarDigital Library
- O'Callahan, R. and Jackson, D. 1997. Lackwit: A program understanding tool based on type inference. In Proceedings of the International Conference on Software Engineering. Google ScholarDigital Library
- Oney, W. 2003. Programming the Microsoft Windows Driver Model. Microsoft Press. Google ScholarDigital Library
- Pande, H. and Ryder, B. 1996. Data-Flow-Based virtual function resolution. In Proceedings of the Static Analysis Symposium. 238--254. Google ScholarDigital Library
- Phoenix. Phoenix software optimization and analysis framework. http://connect.microsoft.com/phoenix.Google Scholar
- Pioli, A. and Hind, M. 1999. Combining interprocedural pointer analysis and conditional constant propagation. Tech. rep. RC 21532(96749), IBM T.J. Watson Research Center.Google Scholar
- PREfast. 2004. PREfast with driver-specific rules. www.microsoft.com/whdc/archive/PREfast-drv.mspx.Google Scholar
- Pugh, W. 1988. Incremental computation and the incremental evaluation of functional programs. Ph.D. thesis, Cornell University. Google ScholarDigital Library
- Ramalingam, G., Field, J., and Tip, F. 1999. Aggregate structure identification and its application to program analysis. In Proceedings of the Symposium on Principles of Programming Languages. Google ScholarDigital Library
- Regehr, J., Reid, A., and Webb, K. 2005. Eliminating stack overflow by abstract interpretation. ACM Trans. Embed. Comput. Syst. 4, 4, 751--778. Google ScholarDigital Library
- Reps, T. and Balakrishnan, G. 2008. Improved memory-access analysis for x86 executables. In Proceedings of the International Conference on Compiler Construction. Google ScholarDigital Library
- Reps, T., Balakrishnan, G., and Lim, J. 2006. Intermediate-Representation recovery from low-level code. In Proceedings of the Conference on Part. Evaluation and Semantics-Based Program Manipulation. Google ScholarDigital Library
- Reps, T., Balakrishnan, G., Lim, J., and Teitelbaum, T. 2005. A next-generation platform for analyzing executables. In Proceedings of the Asian Symposium on Programming Languages and Systems. Google ScholarDigital Library
- Reps, T., Teitelbaum, T., and Demers, A. 1983. Incremental context-dependent analysis for language-based editors. Trans. Program. Lang. Syst. 5, 3, 449--477. Google ScholarDigital Library
- Rival, X. 2003. Abstract interpretation based certification of assembly code. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. Google ScholarDigital Library
- Rugina, R. and Rinard, M. 2005. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. Trans. Program. Lang. Syst. 27, 2, 185--235. Google ScholarDigital Library
- Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ, Chapter 7, 189--234.Google Scholar
- Siff, M. and Reps, T. 1996. Program generalization for software reuse: From C to C++. In Proceedings of the Conference on Foundations of Software Engineering. Google ScholarDigital Library
- Srivastava, A., Edwards, A., and Vo, H. 2001. Vulcan: Binary transformation in a distributed environment. MSR-TR-2001-50, Microsoft Research.Google Scholar
- Srivastava, A. and Eustace, A. 1994. ATOM - A system for building customized program analysis tools. In Proceedings of the Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- Swift, M., Annamalai, M., Bershad, B., and Levy, H. 2004. Recovering device drivers. In Proceedings of the Symposium on Operating Systems Design and Implementation. Google ScholarDigital Library
- Swift, M., Bershad, B., and Levy, H. 2005. Improving the reliability of commodity operating systems. ACM Trans. Comput. Syst. 23, 1. Google ScholarDigital Library
- van Deursen, A. and Moonen, L. 1998. Type inference for COBOL systems. In Proceedings of the Working Conference on Reverse Engineering. Google ScholarDigital Library
- van Deursen, A. and Moonen, L. 1998. Type inference for COBOL systems. In Procedings of the Working Conference on Reverse Engineering. Google ScholarDigital Library
- Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the Conference on Network and Distributed Systems Security.Google Scholar
- Wall, D. 1992. Systems for late code modification. In Code Generation—Concepts, Tools, Techniques, R. Giegerich and S. Graham, Eds. Springer.Google Scholar
- WHDC. 2007. C++ for kernel mode drivers: Pros and cons. www.microsoft.com/whdc/driver/kernel/KMcode.mspx.Google Scholar
- WHQL. 2004. Defrauding the WHQL driver certification process. blogs.msdn.com/oldnewthing/archive/2004/03/05/84469.aspx.Google Scholar
- Wikipedia: Enforceability. Software license agreement: Enforceability (in the United States). en.wikipedia.org/wiki/Software license agreement#Enforceability, Sept. 19, 2009.Google Scholar
- Wikipedia: shrink-wrap and click-wrap licenses. Software license agreement: Shrink-wrap and click-wrap licenses. en.wikipedia.org/wiki/Software license agreement#Shrink-wrap and click-wrap licenses, Sept. 19, 2009.Google Scholar
- Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschu- lat, J., and Stenström, P. 2008. The worst-case execution-time problem—Overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7, 3, 1--53. Google ScholarDigital Library
- Wilson, R. and Lam, M. 1995. Efficient context-sensitive pointer analysis for C programs. In Proceedings of the Conference on Programming Language Design and Implementation. 1--12. Google ScholarDigital Library
- Windows DDK. 2003. Windows Server 2003 DDK. www.microsoft.com/whdc/devtools/ddk.Google Scholar
- Xu, Z., Miller, B., and Reps, T. 2000. Safety checking of machine code. In Proceedings of the Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- Xu, Z., Miller, B., and Reps, T. 2001. Typestate checking of machine code. In Proceedings of the European Symposium on Programming. Google ScholarDigital Library
- Zhang, J., Zhao, R., and Pang, J. 2007. Parameter and return-value analysis of binary executables. In Proceedings of the Computer Software and Applications Conference. Google ScholarDigital Library
Index Terms
- WYSINWYX: What you see is not what you eXecute
Recommendations
A relational approach to interprocedural shape analysis
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three ...
Context transformations for pointer analysis
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationPoints-to analysis for Java benefits greatly from context sensitivity. CFL-reachability and k-limited context strings are two approaches to obtaining context sensitivity with different advantages: CFL-reachability allows local reasoning about data-value ...
Context transformations for pointer analysis
PLDI '17Points-to analysis for Java benefits greatly from context sensitivity. CFL-reachability and k-limited context strings are two approaches to obtaining context sensitivity with different advantages: CFL-reachability allows local reasoning about data-value ...
Comments